COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002		These are some suggestions for changes to the FOL manual designed to
C00013 ENDMK
C⊗;
	These are some suggestions for changes to the FOL manual designed to
make it more useful to its intended users.

Title: The FOL proof checker for first order logic - User's manual

Abstract:

	This manual tells how to use the interactive proof checker FOL.
The axioms of theories expressed in first order logic can be entered
followed by the proofs of propositions.  The proofs can come from files
or can be entered interactively a step at a time.  The logic is a
natural deuction system based on a formulation of Prawitz, but many
extensions have been made including 

	(i) the use of sorts to reduce the size of formulas,
	(ii) the ability to make any purely propositional deduction in one step,
	(iii) the ability to make in one step many deductions involving equality,
	(iv) the ability to verify assertions involving numerical and LISP
constants by calculation,
	(v) the ability to make metamathematical arguments, and
	(vi) many operational conveniences.

	The goal of FOL is to make formal proof a practical tool for checking
proofs in pure mathematics and proofs of the correctness of programs.  It
is also used as a research tool in modeling common sense reasoning
in the representation theory of artificial intelligence.



INTRODUCTION - THE PROBLEM OF PRACTICAL PROOF CHECKING


	The idea of doing mathematical reasoning mechanically goes back to
Leibniz, but
the first completely formal systems adequate for expressing mathematical
reasoning were developed early in this century.  Much of the early work
involved actually developing large parts of mathematics within such as system
and this was carried to its greatest extent in Principia Mathematica by
Whitehead and Russell.  After Principia Mathematica, however, the interest
of mathematicians changed from proving theorems within mathematical systems
to proving meta-theorems about such systems, and this shift in emphasis
persists to the present.

	Even before Godel's work, it was intuitively clear that checking
proofs was different from finding them.  It is an essential part of the
idea of formal system that proofs can be checked mechanically, whereas
finding proofs mechanically was always regarded as a research problem.
This distinction was clarified by the work of Godel, Tarski, Turing and
Church which showed that algorithms for finding proofs can work infallibly
only in limited domains and that some mathematical ideas cannot be
completely characterized by axiomatic systems.

	The advent of computers and the beginning of the study of artificial
intelligence gave rise to attempts to explore experimentally what can
be proved by machine.  There has been steady progress in this endeavor,
but twenty years work leaves us a long way from being able to prove
important mathematical theorems by unaided programs.

	Knowing that mechanical theorem proving has a long way to go justifies
a renewed interest in the simpler task of proof-checking by computer.
Moreover, while it is not as interesting to check proofs by computer
as to make computers prove the theorems, proof-checking has obvious
potential applications.  The most important of these is proving that
computer programs meet their specifications since the reasoning involved
is lengthy although usually straightforward - or so our intuition tells
us.  Moreover, since a computer program is a mathematical object whose
properties are determined entirely by its symbolic form, it is
a mathematical disgrace to have to debug them  case by case rather than proving them
correct in general.  After all mathematical journals don't print papers
consisting of an assertion followed by a vague claim that it seemed
to be correct in a number of cases.  Since the programs are long, the
proofs of correctness would be long, and since programmers sometimes
think wishfully, it is obviously desirable that the proofs be checked
by computer.

	It is also interesting to see if we can check the proofs of
interesting mathematical theorems even though the problem is of less
practical urgency, since the human refereeing process works quite well.

	At first sight, computer proof checking seems almost trivial.
We know that almost all practical mathematical reasoning can be done
in axiomatic set theory which in turn is expressed in first order predicate
calculus.  Therefore, it would seem that all we need do is make a
proof-checker for predicate calculus, choose either the Zermelo-Frankel
or the Godel-Bernays axioms for set theory and write and check our
proofs.  In essence, this is what the FOL project is doing, but in order
to allow formal proofs that are not enormously longer than conventional
mathematical proofs it is necessary to extend the logical mechanisms that
are available in the usual logical systems.

	1. The first order logic allows functions and equality and
infix operators.

	2. The user can declare sorts and declare variables to range over
given sorts.  This greatly reduces the length of axioms and theorems and
corresponds to the fact that in an informal proof a context is established,
and the reader knows that a certain part of the proof is carried out
within the context.

	3. The decision procedures for certain simple domains are built into
the system.  This allows some proofs to be much shorter than usual mathematical
proofs, because the computer can go through some quite complex chains of
reasoning by itself.  At present, propositional deduction and a fragment of
the theory of equality have been implemented.  The Boolean algebra of sets
and elementary commutative algebra are planned.

	4. Some facilities for introducing definitions have been implemented.

	5. Calculations with involving constant individuals and functions
for which algorithms are available can be done directly.  Thus if we
need the fact that 17+34=51, we can get 17+34 directly from the computer
rather than build it up from axioms.  Even more important than such
numerical calculations are symbolic calculations involving LISP expressions
and functions.

	6. Some primitive facilities are available for metamathematical
reasoning.


APPLICATIONS OF COMPUTER PROOF-CHECKING IN FOL

	
	FOL proofs are currently being generated and checked in the following
areas:

	(i) CLASSICAL MATHEMATICS.  This is the most straightforward area
of application, because satisfactory informal proofs are available and
we have only to express them formally.  Several proofs in set theory,
number theory, and group theory have been checked.  Currently many proofs
are about ten times as long as we think they ought to be.  This leads to
improvements in our technique for expressing proofs but also shows where
FOL needs improvement.  We haven't done any metamathematical proofs yet,
and we are far from having a general idea of what concepts are used
by mathematicians.

	(ii) MATHEMATICAL THEORY OF COMPUTATION.